\begin{tabbing}
weakPrecondSendR\{\$a,\$tg\}($T$;$A$;$l$;${\it ds}$;$P$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=[@source($l$) \=precondition for "\$a"(v:$A$):\+\+
\\[0ex]$P$ State(${\it ds}$) v
\-\\[0ex]; \=sends locl("\$a")(v:$A$) on $l$:\+
\\[0ex]tagged($\langle$"\$tg"$,\,$$\lambda$$s$,$v$. ($f$($s$,$v$)).nil$\rangle$.nil,State(${\it ds}$),v):"\$tg" : $T$
\-\\[0ex]/ only events in locl("\$a").nil send on $l$ with "\$tg".nil])
\-
\end{tabbing}